(set-logic QF_BV)
(declare-fun x () (_ BitVec 28))
(declare-fun b1 () Bool)
(declare-fun b2 () Bool)
(declare-fun b3 () Bool)
(declare-fun b4 () Bool)
(declare-fun b5 () Bool)
(declare-fun b6 () Bool)
(declare-fun b7 () Bool)
(declare-fun b8 () Bool)
(declare-fun b9 () Bool)
(declare-fun b10 () Bool)
(declare-fun b11 () Bool)
(declare-fun b12 () Bool)
(declare-fun v0 () (_ BitVec 12))
(declare-fun v2 () (_ BitVec 13))
(declare-fun v4 () (_ BitVec 22))
(assert
  (let ((e42 (bvmul (ite (bvsge v4 (_ bv0 22)) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 15) v2) x) (_ bv1 1) (_ bv0 1)))))
  (let ((e524 (not (=> (not (= ((_ sign_extend 12) e42) (bvnand (_ bv0 13) (_ bv0 13)))) b12)))) (and (and (and (and (and (and (and (and (and (and (= (xor (bvsge (_ bv0 13) v2) (not (or (not (= ((_ zero_extend 2) v0) (bvmul ((_ zero_extend 13) e42) ((_ sign_extend 13) e42)))) b1))) (not (=> (not (= ((_ sign_extend 12) e42) (bvnand (_ bv0 13) (_ bv0 13)))) b12))) b6) b7) b2) b8) b3) b4) b5) b9) b10) b11))))
(check-sat)

